Nuprl Definition : es_realizer_ind_Rnone_compseq_tag_def
0,22
postcript
pdf
es_realizer_ind_Rnone{
es
realizer
ind
Rnone
compseq
tag
def
:ObjectId}
es_realizer_ind_Rnone
(
v11
,
v12
,
v13
.
rframe
(
v11
;
v12
;
v13
);
es_realizer_ind_Rnone(
v21
,
v22
,
v23
.
bframe
(
v21
;
v22
;
v23
);
es_realizer_ind_Rnone(
v31
,
v32
,
v33
.
aframe
(
v31
;
v32
;
v33
);
es_realizer_ind_Rnone(
v41
,
v42
,
v43
,
v44
,
v45
.
pre
(
v41
;
v42
;
v43
;
v44
;
v45
);
es_realizer_ind_Rnone(
v51
,
v52
,
v53
,
v54
,
v55
,
v56
.
sends
(
v51
;
v52
;
v53
;
v54
;
v55
;
v56
);
es_realizer_ind_Rnone(
v61
,
v62
,
v63
,
v64
,
v65
,
v66
.
effect
(
v61
;
v62
;
v63
;
v64
;
v65
;
v66
);
es_realizer_ind_Rnone(
v71
,
v72
,
v73
.
sframe
(
v71
;
v72
;
v73
);
es_realizer_ind_Rnone(
v81
,
v82
,
v83
,
v84
.
frame
(
v81
;
v82
;
v83
;
v84
);
es_realizer_ind_Rnone(
v91
,
v92
,
v93
,
v94
.
init
(
v91
;
v92
;
v93
;
v94
);
es_realizer_ind_Rnone(
v101
,
v102
,
v103
,
v104
.
plus
(
v101
;
v102
;
v103
;
v104
);
es_realizer_ind_Rnone(
none
)
== compseq(case
of
== compseq(
Rnone =>
none
== compseq(
Rplus(
left
,
right
)=>
rec1
,
rec2
.
plus
(
left
;
right
;
rec1
;
rec2
)
== compseq(
Rinit(
loc
,
T
,
x
,
v
)=>
init
(
loc
;
T
;
x
;
v
)
== compseq(
Rframe(
loc
,
T
,
x
,
L
)=>
frame
(
loc
;
T
;
x
;
L
)
== compseq(
Rsframe(
lnk
,
tag
,
L
)=>
sframe
(
lnk
;
tag
;
L
)
== compseq(
Reffect(
loc
,
ds
,
knd
,
T
,
x
,
f
)=>
effect
(
loc
;
ds
;
knd
;
T
;
x
;
f
)
== compseq(
Rsends(
ds
,
knd
,
T
,
l
,
dt
,
g
)=>
sends
(
ds
;
knd
;
T
;
l
;
dt
;
g
)
== compseq(
Rpre(
loc
,
ds
,
a
,
T
,
P
)=>
pre
(
loc
;
ds
;
a
;
T
;
P
)
== compseq(
Raframe(
loc
,
k
,
L
)=>
aframe
(
loc
;
k
;
L
)
== compseq(
Rbframe(
loc
,
k
,
L
)=>
bframe
(
loc
;
k
;
L
)
== compseq(
Rrframe(
loc
,
x
,
L
)=>
rframe
(
loc
;
x
;
L
);
== compseq(
none
)
latex
Definitions
es
realizer
ind
,
origin